Nuprl Lemma : lnk-inv-one-one
11,40
postcript
pdf
l1
,
l2
:IdLnk. (lnk-inv(
l1
) = lnk-inv(
l2
)
IdLnk)
(
l1
=
l2
)
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
t
T
,
,
SQType(
T
)
,
{
T
}
Lemmas
IdLnk
wf
,
lnk-inv
wf
,
lnk-inv-inv
,
IdLnk
sq
origin
l1, l2:IdLnk. (lnk-inv(l1) = lnk-inv(l2) 
IdLnk) 
(l1 = l2) l1, l2:IdLnk. (lnk-inv(l1) = lnk-inv(l2) IdLnk) (l1 = l2) x:A. B(x) Q Q Q T